ds:(IdType), da:(IdKndType), A, B:Type, X:Interface(ds;da;A), Y:Interface(ds;da;B), es:ES.
es-decl(es;ds;da)
 [[X]]  [[Y]] = 0
 (es-interface-right([[interface-union(X;Y)]]) = [[Y]]  AbsInterface(B)) 

latex

Definitions

s ~ t, interface-union(X;Y), p q, in-interface(es;X;e), Knd, Id, Type, Interface(ds;da;A), ES, es-decl(es;ds;da), <a, b>, f(a), X  Y = 0, e  X, f o g  , can-apply(f;x), do-apply(f;x), b, es-interface-right(X), P  Q, x:A. B(x), s = t, [[X]], t  T, x:AB(x), left + right, Top, E, AbsInterface(A), LocKnd, loc(e), kind(e), x  dom(f), SQType(T), {T}, , deq-member(eq;x;L), hasloc(k;i), t.1, A, False, a:A fp B(a), {x:A| B(x)} , x:A  B(x), let x,y = A in B(x;y), type List, fpf-domain(f), x. t(x), x.A(x), let i,k:LocKnd = ik in P(i;k), x,y. t(x;y), locknd-deq(), as @ bs, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , , P  Q, (x  l), P  Q, P & Q, P  Q, t.2, (state when e), val(e), interface-val(es;X;e), f(x), x:A.B(x), Void, Unit, isl(x), outl(x), inl x , inr x , True, invert-union(x), ff

Lemmas

interface-val wf, not wf, isl wf, assert of bnot, eqff to assert, eqtt to assert, equal-top, member append, l member wf, assert-deq-member, or functionality wrt iff, assert of bor, iff transitivity, deq-member wf, bor wf, append wf, locknd-deq wf, LocKnd wf, iff imp equal bool, top wf, locknd-spread wf2, fpf-trivial-subtype-top, fpf-domain wf, Knd wf, Id wf, hasloc wf, assert wf, es-hasloc, es-kind wf, es-loc wf, bool sq, abs-interface wf, es-interface-right wf